Left Termination proof of /tmp/tmpQ7odCk/pl4.4.3.pl

Left Termination of the query pattern merge_in_3(g, g, a) w.r.t. the given Prolog program could successfully be proven:

↳ Prolog

  ↳ PrologToPiTRSProof

Clauses:

merge(X, [], X).
merge([], X, X).
merge(.(A, X), .(B, Y), .(A, Z)) :- ','(le(A, B), merge(X, .(B, Y), Z)).
merge(.(A, X), .(B, Y), .(B, Z)) :- ','(gt(A, B), merge(.(A, X), Y, Z)).
gt(s(X), s(Y)) :- gt(X, Y).
gt(s(X), zero).
le(s(X), s(Y)) :- le(X, Y).
le(zero, s(Y)).
le(zero, zero).

Queries:

merge(g,g,a).

We use the technique of [30].Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

merge_in(.(A, X), .(B, Y), .(B, Z)) → U3(A, X, B, Y, Z, gt_in(A, B))
gt_in(s(X), zero) → gt_out(s(X), zero)
gt_in(s(X), s(Y)) → U5(X, Y, gt_in(X, Y))
U5(X, Y, gt_out(X, Y)) → gt_out(s(X), s(Y))
U3(A, X, B, Y, Z, gt_out(A, B)) → U4(A, X, B, Y, Z, merge_in(.(A, X), Y, Z))
merge_in(.(A, X), .(B, Y), .(A, Z)) → U1(A, X, B, Y, Z, le_in(A, B))
le_in(zero, zero) → le_out(zero, zero)
le_in(zero, s(Y)) → le_out(zero, s(Y))
le_in(s(X), s(Y)) → U6(X, Y, le_in(X, Y))
U6(X, Y, le_out(X, Y)) → le_out(s(X), s(Y))
U1(A, X, B, Y, Z, le_out(A, B)) → U2(A, X, B, Y, Z, merge_in(X, .(B, Y), Z))
merge_in([], X, X) → merge_out([], X, X)
merge_in(X, [], X) → merge_out(X, [], X)
U2(A, X, B, Y, Z, merge_out(X, .(B, Y), Z)) → merge_out(.(A, X), .(B, Y), .(A, Z))
U4(A, X, B, Y, Z, merge_out(.(A, X), Y, Z)) → merge_out(.(A, X), .(B, Y), .(B, Z))

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

merge_in(.(A, X), .(B, Y), .(B, Z)) → U3(A, X, B, Y, Z, gt_in(A, B))
gt_in(s(X), zero) → gt_out(s(X), zero)
gt_in(s(X), s(Y)) → U5(X, Y, gt_in(X, Y))
U5(X, Y, gt_out(X, Y)) → gt_out(s(X), s(Y))
U3(A, X, B, Y, Z, gt_out(A, B)) → U4(A, X, B, Y, Z, merge_in(.(A, X), Y, Z))
merge_in(.(A, X), .(B, Y), .(A, Z)) → U1(A, X, B, Y, Z, le_in(A, B))
le_in(zero, zero) → le_out(zero, zero)
le_in(zero, s(Y)) → le_out(zero, s(Y))
le_in(s(X), s(Y)) → U6(X, Y, le_in(X, Y))
U6(X, Y, le_out(X, Y)) → le_out(s(X), s(Y))
U1(A, X, B, Y, Z, le_out(A, B)) → U2(A, X, B, Y, Z, merge_in(X, .(B, Y), Z))
merge_in([], X, X) → merge_out([], X, X)
merge_in(X, [], X) → merge_out(X, [], X)
U2(A, X, B, Y, Z, merge_out(X, .(B, Y), Z)) → merge_out(.(A, X), .(B, Y), .(A, Z))
U4(A, X, B, Y, Z, merge_out(.(A, X), Y, Z)) → merge_out(.(A, X), .(B, Y), .(B, Z))

MERGE_IN(.(A, X), .(B, Y), .(B, Z)) → U3¹(A, X, B, Y, Z, gt_in(A, B))
MERGE_IN(.(A, X), .(B, Y), .(B, Z)) → GT_IN(A, B)
GT_IN(s(X), s(Y)) → U5¹(X, Y, gt_in(X, Y))
GT_IN(s(X), s(Y)) → GT_IN(X, Y)
U3¹(A, X, B, Y, Z, gt_out(A, B)) → U4¹(A, X, B, Y, Z, merge_in(.(A, X), Y, Z))
U3¹(A, X, B, Y, Z, gt_out(A, B)) → MERGE_IN(.(A, X), Y, Z)
MERGE_IN(.(A, X), .(B, Y), .(A, Z)) → U1¹(A, X, B, Y, Z, le_in(A, B))
MERGE_IN(.(A, X), .(B, Y), .(A, Z)) → LE_IN(A, B)
LE_IN(s(X), s(Y)) → U6¹(X, Y, le_in(X, Y))
LE_IN(s(X), s(Y)) → LE_IN(X, Y)
U1¹(A, X, B, Y, Z, le_out(A, B)) → U2¹(A, X, B, Y, Z, merge_in(X, .(B, Y), Z))
U1¹(A, X, B, Y, Z, le_out(A, B)) → MERGE_IN(X, .(B, Y), Z)

The TRS R consists of the following rules:

merge_in(.(A, X), .(B, Y), .(B, Z)) → U3(A, X, B, Y, Z, gt_in(A, B))
gt_in(s(X), zero) → gt_out(s(X), zero)
gt_in(s(X), s(Y)) → U5(X, Y, gt_in(X, Y))
U5(X, Y, gt_out(X, Y)) → gt_out(s(X), s(Y))
U3(A, X, B, Y, Z, gt_out(A, B)) → U4(A, X, B, Y, Z, merge_in(.(A, X), Y, Z))
merge_in(.(A, X), .(B, Y), .(A, Z)) → U1(A, X, B, Y, Z, le_in(A, B))
le_in(zero, zero) → le_out(zero, zero)
le_in(zero, s(Y)) → le_out(zero, s(Y))
le_in(s(X), s(Y)) → U6(X, Y, le_in(X, Y))
U6(X, Y, le_out(X, Y)) → le_out(s(X), s(Y))
U1(A, X, B, Y, Z, le_out(A, B)) → U2(A, X, B, Y, Z, merge_in(X, .(B, Y), Z))
merge_in([], X, X) → merge_out([], X, X)
merge_in(X, [], X) → merge_out(X, [], X)
U2(A, X, B, Y, Z, merge_out(X, .(B, Y), Z)) → merge_out(.(A, X), .(B, Y), .(A, Z))
U4(A, X, B, Y, Z, merge_out(.(A, X), Y, Z)) → merge_out(.(A, X), .(B, Y), .(B, Z))

The argument filtering Pi contains the following mapping:
merge_in(x1, x2, x3) = merge_in(x1, x2)
.(x1, x2) = .(x1, x2)
U3(x1, x2, x3, x4, x5, x6) = U3(x1, x2, x3, x4, x6)
gt_in(x1, x2) = gt_in(x1, x2)
s(x1) = s(x1)
zero = zero
gt_out(x1, x2) = gt_out
U5(x1, x2, x3) = U5(x3)
U4(x1, x2, x3, x4, x5, x6) = U4(x3, x6)
U1(x1, x2, x3, x4, x5, x6) = U1(x1, x2, x3, x4, x6)
le_in(x1, x2) = le_in(x1, x2)
le_out(x1, x2) = le_out
U6(x1, x2, x3) = U6(x3)
U2(x1, x2, x3, x4, x5, x6) = U2(x1, x6)
[] = []
merge_out(x1, x2, x3) = merge_out(x3)
U6¹(x1, x2, x3) = U6¹(x3)
U5¹(x1, x2, x3) = U5¹(x3)
MERGE_IN(x1, x2, x3) = MERGE_IN(x1, x2)
U2¹(x1, x2, x3, x4, x5, x6) = U2¹(x1, x6)
U4¹(x1, x2, x3, x4, x5, x6) = U4¹(x3, x6)
LE_IN(x1, x2) = LE_IN(x1, x2)
U1¹(x1, x2, x3, x4, x5, x6) = U1¹(x1, x2, x3, x4, x6)
GT_IN(x1, x2) = GT_IN(x1, x2)
U3¹(x1, x2, x3, x4, x5, x6) = U3¹(x1, x2, x3, x4, x6)

We have to consider all (P,R,Pi)-chains

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

MERGE_IN(.(A, X), .(B, Y), .(B, Z)) → U3¹(A, X, B, Y, Z, gt_in(A, B))
MERGE_IN(.(A, X), .(B, Y), .(B, Z)) → GT_IN(A, B)
GT_IN(s(X), s(Y)) → U5¹(X, Y, gt_in(X, Y))
GT_IN(s(X), s(Y)) → GT_IN(X, Y)
U3¹(A, X, B, Y, Z, gt_out(A, B)) → U4¹(A, X, B, Y, Z, merge_in(.(A, X), Y, Z))
U3¹(A, X, B, Y, Z, gt_out(A, B)) → MERGE_IN(.(A, X), Y, Z)
MERGE_IN(.(A, X), .(B, Y), .(A, Z)) → U1¹(A, X, B, Y, Z, le_in(A, B))
MERGE_IN(.(A, X), .(B, Y), .(A, Z)) → LE_IN(A, B)
LE_IN(s(X), s(Y)) → U6¹(X, Y, le_in(X, Y))
LE_IN(s(X), s(Y)) → LE_IN(X, Y)
U1¹(A, X, B, Y, Z, le_out(A, B)) → U2¹(A, X, B, Y, Z, merge_in(X, .(B, Y), Z))
U1¹(A, X, B, Y, Z, le_out(A, B)) → MERGE_IN(X, .(B, Y), Z)

The TRS R consists of the following rules:

merge_in(.(A, X), .(B, Y), .(B, Z)) → U3(A, X, B, Y, Z, gt_in(A, B))
gt_in(s(X), zero) → gt_out(s(X), zero)
gt_in(s(X), s(Y)) → U5(X, Y, gt_in(X, Y))
U5(X, Y, gt_out(X, Y)) → gt_out(s(X), s(Y))
U3(A, X, B, Y, Z, gt_out(A, B)) → U4(A, X, B, Y, Z, merge_in(.(A, X), Y, Z))
merge_in(.(A, X), .(B, Y), .(A, Z)) → U1(A, X, B, Y, Z, le_in(A, B))
le_in(zero, zero) → le_out(zero, zero)
le_in(zero, s(Y)) → le_out(zero, s(Y))
le_in(s(X), s(Y)) → U6(X, Y, le_in(X, Y))
U6(X, Y, le_out(X, Y)) → le_out(s(X), s(Y))
U1(A, X, B, Y, Z, le_out(A, B)) → U2(A, X, B, Y, Z, merge_in(X, .(B, Y), Z))
merge_in([], X, X) → merge_out([], X, X)
merge_in(X, [], X) → merge_out(X, [], X)
U2(A, X, B, Y, Z, merge_out(X, .(B, Y), Z)) → merge_out(.(A, X), .(B, Y), .(A, Z))
U4(A, X, B, Y, Z, merge_out(.(A, X), Y, Z)) → merge_out(.(A, X), .(B, Y), .(B, Z))

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

LE_IN(s(X), s(Y)) → LE_IN(X, Y)

The TRS R consists of the following rules:

merge_in(.(A, X), .(B, Y), .(B, Z)) → U3(A, X, B, Y, Z, gt_in(A, B))
gt_in(s(X), zero) → gt_out(s(X), zero)
gt_in(s(X), s(Y)) → U5(X, Y, gt_in(X, Y))
U5(X, Y, gt_out(X, Y)) → gt_out(s(X), s(Y))
U3(A, X, B, Y, Z, gt_out(A, B)) → U4(A, X, B, Y, Z, merge_in(.(A, X), Y, Z))
merge_in(.(A, X), .(B, Y), .(A, Z)) → U1(A, X, B, Y, Z, le_in(A, B))
le_in(zero, zero) → le_out(zero, zero)
le_in(zero, s(Y)) → le_out(zero, s(Y))
le_in(s(X), s(Y)) → U6(X, Y, le_in(X, Y))
U6(X, Y, le_out(X, Y)) → le_out(s(X), s(Y))
U1(A, X, B, Y, Z, le_out(A, B)) → U2(A, X, B, Y, Z, merge_in(X, .(B, Y), Z))
merge_in([], X, X) → merge_out([], X, X)
merge_in(X, [], X) → merge_out(X, [], X)
U2(A, X, B, Y, Z, merge_out(X, .(B, Y), Z)) → merge_out(.(A, X), .(B, Y), .(A, Z))
U4(A, X, B, Y, Z, merge_out(.(A, X), Y, Z)) → merge_out(.(A, X), .(B, Y), .(B, Z))

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

LE_IN(s(X), s(Y)) → LE_IN(X, Y)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

LE_IN(s(X), s(Y)) → LE_IN(X, Y)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

LE_IN(s(X), s(Y)) → LE_IN(X, Y)
The graph contains the following edges 1 > 1, 2 > 2

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

GT_IN(s(X), s(Y)) → GT_IN(X, Y)

The TRS R consists of the following rules:

merge_in(.(A, X), .(B, Y), .(B, Z)) → U3(A, X, B, Y, Z, gt_in(A, B))
gt_in(s(X), zero) → gt_out(s(X), zero)
gt_in(s(X), s(Y)) → U5(X, Y, gt_in(X, Y))
U5(X, Y, gt_out(X, Y)) → gt_out(s(X), s(Y))
U3(A, X, B, Y, Z, gt_out(A, B)) → U4(A, X, B, Y, Z, merge_in(.(A, X), Y, Z))
merge_in(.(A, X), .(B, Y), .(A, Z)) → U1(A, X, B, Y, Z, le_in(A, B))
le_in(zero, zero) → le_out(zero, zero)
le_in(zero, s(Y)) → le_out(zero, s(Y))
le_in(s(X), s(Y)) → U6(X, Y, le_in(X, Y))
U6(X, Y, le_out(X, Y)) → le_out(s(X), s(Y))
U1(A, X, B, Y, Z, le_out(A, B)) → U2(A, X, B, Y, Z, merge_in(X, .(B, Y), Z))
merge_in([], X, X) → merge_out([], X, X)
merge_in(X, [], X) → merge_out(X, [], X)
U2(A, X, B, Y, Z, merge_out(X, .(B, Y), Z)) → merge_out(.(A, X), .(B, Y), .(A, Z))
U4(A, X, B, Y, Z, merge_out(.(A, X), Y, Z)) → merge_out(.(A, X), .(B, Y), .(B, Z))

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

GT_IN(s(X), s(Y)) → GT_IN(X, Y)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

GT_IN(s(X), s(Y)) → GT_IN(X, Y)

From the DPs we obtained the following set of size-change graphs:

GT_IN(s(X), s(Y)) → GT_IN(X, Y)
The graph contains the following edges 1 > 1, 2 > 2

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

Pi DP problem:
The TRS P consists of the following rules:

MERGE_IN(.(A, X), .(B, Y), .(A, Z)) → U1¹(A, X, B, Y, Z, le_in(A, B))
U1¹(A, X, B, Y, Z, le_out(A, B)) → MERGE_IN(X, .(B, Y), Z)
MERGE_IN(.(A, X), .(B, Y), .(B, Z)) → U3¹(A, X, B, Y, Z, gt_in(A, B))
U3¹(A, X, B, Y, Z, gt_out(A, B)) → MERGE_IN(.(A, X), Y, Z)

The TRS R consists of the following rules:

merge_in(.(A, X), .(B, Y), .(B, Z)) → U3(A, X, B, Y, Z, gt_in(A, B))
gt_in(s(X), zero) → gt_out(s(X), zero)
gt_in(s(X), s(Y)) → U5(X, Y, gt_in(X, Y))
U5(X, Y, gt_out(X, Y)) → gt_out(s(X), s(Y))
U3(A, X, B, Y, Z, gt_out(A, B)) → U4(A, X, B, Y, Z, merge_in(.(A, X), Y, Z))
merge_in(.(A, X), .(B, Y), .(A, Z)) → U1(A, X, B, Y, Z, le_in(A, B))
le_in(zero, zero) → le_out(zero, zero)
le_in(zero, s(Y)) → le_out(zero, s(Y))
le_in(s(X), s(Y)) → U6(X, Y, le_in(X, Y))
U6(X, Y, le_out(X, Y)) → le_out(s(X), s(Y))
U1(A, X, B, Y, Z, le_out(A, B)) → U2(A, X, B, Y, Z, merge_in(X, .(B, Y), Z))
merge_in([], X, X) → merge_out([], X, X)
merge_in(X, [], X) → merge_out(X, [], X)
U2(A, X, B, Y, Z, merge_out(X, .(B, Y), Z)) → merge_out(.(A, X), .(B, Y), .(A, Z))
U4(A, X, B, Y, Z, merge_out(.(A, X), Y, Z)) → merge_out(.(A, X), .(B, Y), .(B, Z))

The argument filtering Pi contains the following mapping:
merge_in(x1, x2, x3) = merge_in(x1, x2)
.(x1, x2) = .(x1, x2)
U3(x1, x2, x3, x4, x5, x6) = U3(x1, x2, x3, x4, x6)
gt_in(x1, x2) = gt_in(x1, x2)
s(x1) = s(x1)
zero = zero
gt_out(x1, x2) = gt_out
U5(x1, x2, x3) = U5(x3)
U4(x1, x2, x3, x4, x5, x6) = U4(x3, x6)
U1(x1, x2, x3, x4, x5, x6) = U1(x1, x2, x3, x4, x6)
le_in(x1, x2) = le_in(x1, x2)
le_out(x1, x2) = le_out
U6(x1, x2, x3) = U6(x3)
U2(x1, x2, x3, x4, x5, x6) = U2(x1, x6)
[] = []
merge_out(x1, x2, x3) = merge_out(x3)
MERGE_IN(x1, x2, x3) = MERGE_IN(x1, x2)
U1¹(x1, x2, x3, x4, x5, x6) = U1¹(x1, x2, x3, x4, x6)
U3¹(x1, x2, x3, x4, x5, x6) = U3¹(x1, x2, x3, x4, x6)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

MERGE_IN(.(A, X), .(B, Y), .(A, Z)) → U1¹(A, X, B, Y, Z, le_in(A, B))
U1¹(A, X, B, Y, Z, le_out(A, B)) → MERGE_IN(X, .(B, Y), Z)
MERGE_IN(.(A, X), .(B, Y), .(B, Z)) → U3¹(A, X, B, Y, Z, gt_in(A, B))
U3¹(A, X, B, Y, Z, gt_out(A, B)) → MERGE_IN(.(A, X), Y, Z)

The TRS R consists of the following rules:

le_in(zero, zero) → le_out(zero, zero)
le_in(zero, s(Y)) → le_out(zero, s(Y))
le_in(s(X), s(Y)) → U6(X, Y, le_in(X, Y))
gt_in(s(X), zero) → gt_out(s(X), zero)
gt_in(s(X), s(Y)) → U5(X, Y, gt_in(X, Y))
U6(X, Y, le_out(X, Y)) → le_out(s(X), s(Y))
U5(X, Y, gt_out(X, Y)) → gt_out(s(X), s(Y))

The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
gt_in(x1, x2) = gt_in(x1, x2)
s(x1) = s(x1)
zero = zero
gt_out(x1, x2) = gt_out
U5(x1, x2, x3) = U5(x3)
le_in(x1, x2) = le_in(x1, x2)
le_out(x1, x2) = le_out
U6(x1, x2, x3) = U6(x3)
MERGE_IN(x1, x2, x3) = MERGE_IN(x1, x2)
U1¹(x1, x2, x3, x4, x5, x6) = U1¹(x1, x2, x3, x4, x6)
U3¹(x1, x2, x3, x4, x5, x6) = U3¹(x1, x2, x3, x4, x6)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

U1¹(A, X, B, Y, le_out) → MERGE_IN(X, .(B, Y))
MERGE_IN(.(A, X), .(B, Y)) → U1¹(A, X, B, Y, le_in(A, B))
MERGE_IN(.(A, X), .(B, Y)) → U3¹(A, X, B, Y, gt_in(A, B))
U3¹(A, X, B, Y, gt_out) → MERGE_IN(.(A, X), Y)

The TRS R consists of the following rules:

le_in(zero, zero) → le_out
le_in(zero, s(Y)) → le_out
le_in(s(X), s(Y)) → U6(le_in(X, Y))
gt_in(s(X), zero) → gt_out
gt_in(s(X), s(Y)) → U5(gt_in(X, Y))
U6(le_out) → le_out
U5(gt_out) → gt_out

The set Q consists of the following terms:

le_in(x0, x1)
gt_in(x0, x1)
U6(x0)
U5(x0)

We have to consider all (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

U3¹(A, X, B, Y, gt_out) → MERGE_IN(.(A, X), Y)

The remaining pairs can at least be oriented weakly.

U1¹(A, X, B, Y, le_out) → MERGE_IN(X, .(B, Y))
MERGE_IN(.(A, X), .(B, Y)) → U1¹(A, X, B, Y, le_in(A, B))
MERGE_IN(.(A, X), .(B, Y)) → U3¹(A, X, B, Y, gt_in(A, B))

Used ordering: Combined order from the following AFS and order.
U1¹(x1, x2, x3, x4, x5) = U1¹(x3, x4)
le_out = le_out
MERGE_IN(x1, x2) = x2
.(x1, x2) = .(x1, x2)
le_in(x1, x2) = x1
U3¹(x1, x2, x3, x4, x5) = U3¹(x4, x5)
gt_in(x1, x2) = gt_in
gt_out = gt_out
zero = zero
U6(x1) = U6(x1)
s(x1) = s
U5(x1) = x1

Recursive path order with status [2].
Quasi-Precedence:

[U1^1₂, le_out, .₂, U3^1_2] > [gt_in, gt_out]
zero > [gt_in, gt_out]
s > U6₁ > [gt_in, gt_out]

Status:

U6₁: multiset
le_out: multiset
zero: multiset
U3^1₂: multiset
U1^1₂: multiset
s: multiset
.₂: multiset
gt_in: []
gt_out: multiset

The following usable rules [17] were oriented:

gt_in(s(X), zero) → gt_out
U5(gt_out) → gt_out
gt_in(s(X), s(Y)) → U5(gt_in(X, Y))

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

MERGE_IN(.(A, X), .(B, Y)) → U1¹(A, X, B, Y, le_in(A, B))
U1¹(A, X, B, Y, le_out) → MERGE_IN(X, .(B, Y))
MERGE_IN(.(A, X), .(B, Y)) → U3¹(A, X, B, Y, gt_in(A, B))

The TRS R consists of the following rules:

le_in(zero, zero) → le_out
le_in(zero, s(Y)) → le_out
le_in(s(X), s(Y)) → U6(le_in(X, Y))
gt_in(s(X), zero) → gt_out
gt_in(s(X), s(Y)) → U5(gt_in(X, Y))
U6(le_out) → le_out
U5(gt_out) → gt_out

The set Q consists of the following terms:

le_in(x0, x1)
gt_in(x0, x1)
U6(x0)
U5(x0)

We have to consider all (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

U1¹(A, X, B, Y, le_out) → MERGE_IN(X, .(B, Y))
MERGE_IN(.(A, X), .(B, Y)) → U1¹(A, X, B, Y, le_in(A, B))

The TRS R consists of the following rules:

le_in(zero, zero) → le_out
le_in(zero, s(Y)) → le_out
le_in(s(X), s(Y)) → U6(le_in(X, Y))
gt_in(s(X), zero) → gt_out
gt_in(s(X), s(Y)) → U5(gt_in(X, Y))
U6(le_out) → le_out
U5(gt_out) → gt_out

The set Q consists of the following terms:

le_in(x0, x1)
gt_in(x0, x1)
U6(x0)
U5(x0)

We have to consider all (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

U1¹(A, X, B, Y, le_out) → MERGE_IN(X, .(B, Y))
MERGE_IN(.(A, X), .(B, Y)) → U1¹(A, X, B, Y, le_in(A, B))

The TRS R consists of the following rules:

le_in(zero, zero) → le_out
le_in(zero, s(Y)) → le_out
le_in(s(X), s(Y)) → U6(le_in(X, Y))
U6(le_out) → le_out

The set Q consists of the following terms:

le_in(x0, x1)
gt_in(x0, x1)
U6(x0)
U5(x0)

We have to consider all (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

gt_in(x0, x1)
U5(x0)

↳ Prolog

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

MERGE_IN(.(A, X), .(B, Y)) → U1¹(A, X, B, Y, le_in(A, B))
U1¹(A, X, B, Y, le_out) → MERGE_IN(X, .(B, Y))

The TRS R consists of the following rules:

le_in(zero, zero) → le_out
le_in(zero, s(Y)) → le_out
le_in(s(X), s(Y)) → U6(le_in(X, Y))
U6(le_out) → le_out

The set Q consists of the following terms:

le_in(x0, x1)
U6(x0)

We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

MERGE_IN(.(A, X), .(B, Y)) → U1¹(A, X, B, Y, le_in(A, B))
The graph contains the following edges 1 > 1, 1 > 2, 2 > 3, 2 > 4
U1¹(A, X, B, Y, le_out) → MERGE_IN(X, .(B, Y))
The graph contains the following edges 2 >= 1